\begin{tabbing}
$M$.rframe($A$.sends ${\it tfL}$ of $k$ on $l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=IdIdDeq$\forall$$x$$\in$dom(($M$.2.2.2.2.2.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]$L$\==($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ \+
\\[0ex]($\uparrow$deq{-}member(KindDeq;$k$;$L$))
\-\\[0ex]$\vee$ \=($\forall$$s_{1}$:$A$.state, $s_{2}$:$A$.state, $v$:$A$.da($k$).\+
\\[0ex]ma{-}x{-}equiv($A$;$x$;$s_{1}$;$s_{2}$)
\\[0ex]$\Rightarrow$ \=($\forall$$i$:\{0..$\parallel$${\it tfL}$$\parallel^{-}$\}.\+
\\[0ex](${\it tfL}$[$i$].2)($s_{1}$,$v$) = (${\it tfL}$[$i$].2)($s_{2}$,$v$) $\in$ ($A$.dout($l$,${\it tfL}$[$i$].1) List)))
\-\-\-
\end{tabbing}